<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
            "http://www.w3.org/TR/REC-html40/loose.dtd">
<HTML>
<HEAD>



<META http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
<META name="GENERATOR" content="hevea 1.08">
<LINK rel="stylesheet" type="text/css" href="libman.css">
<TITLE>
Introduction
</TITLE>
</HEAD>
<BODY >
<A HREF="libman016.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman018.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
<HR>

<H2 CLASS="section"><A NAME="htoc26">3.1</A>&nbsp;&nbsp;Introduction</H2><UL>
<LI><A HREF="libman017.html#toc11">What IC does</A>
<LI><A HREF="libman017.html#toc12">Differences between IC and FD</A>
<LI><A HREF="libman017.html#toc13">Differences between IC and RIA</A>
<LI><A HREF="libman017.html#toc14">Notes about interval arithmetic</A>
<LI><A HREF="libman017.html#toc15">Interval arithmetic and IC</A>
<LI><A HREF="libman017.html#toc16">Usage</A>
<LI><A HREF="libman017.html#toc17">Arithmetic Expressions</A>
</UL>

The IC (Interval Constraint) library is a hybrid integer/real interval
arithmetic constraint solver. Its aim is to make it convenient for
programmers to write hybrid solutions to problems, mixing together integer
and real constraints and variables.<BR>
<BR>
Previously, if one wished to mix integer and real constraints, one had to
import separate solvers for each, with the solvers using different
representations for the domains of variables. This meant any variable
appearing in both kinds of constraints would end up with two domain
representations, with extra constraints necessary to keep the two
representations synchronised.<BR>
<BR>
<A NAME="toc11"></A>
<H3 CLASS="subsection"><A NAME="htoc27">3.1.1</A>&nbsp;&nbsp;What IC does</H3>
<A NAME="@default6"></A>
IC is a general interval propagation solver which can be used to solve
problems over both integer and real variables. Integer variables behave
much like those from the old finite domain solver FD, while real variables
behave much like those from the old real interval arithmetic solver RIA.
IC allows both kinds of variables to be mixed seamlessly in constraints,
since (with a few exceptions) the same propagation algorithms are used
throughout and all variables have the same underlying representation
(indeed, a real variable can be turned into an integer variable simply by
imposing an integrality constraint on it).<BR>
<BR>
IC replaces the `fd', `ria' and `range' libraries. Since IC does not
support symbolic domains, there is a separate symbolic solver library
`ic_symbolic', to provide the non-numeric functionality of `fd'.<BR>
<BR>
<A NAME="toc12"></A>
<H3 CLASS="subsection"><A NAME="htoc28">3.1.2</A>&nbsp;&nbsp;Differences between IC and FD</H3>
<UL CLASS="itemize"><LI CLASS="li-itemize">
IC supports real variables and constraints; FD does not.<BR>
<BR>
<LI CLASS="li-itemize">FD supports symbolic domains; IC does not (use the ic_symbolic
 library).<BR>
<BR>
<LI CLASS="li-itemize">In FD, numeric domains are more or less limited to
 -10000000..10000000 (this default domain can be modified, but the
 larger one makes it, the more likely one is to run into machine
 integer overflow problems). In IC there is no limit as such, and
 bounds on integer variables can be infinite (though variables should
 not be assigned infinite values). However, since floating point
 numbers are used in the underlying implementation, not every integer
 value is representable. Specifically, integer variables and
 constraints ought to behave as expected until the values being
 manipulated become large enough that they approach the precision
 limit of a double precision floating point number (2<SUP>51</SUP> or so).
 Beyond this, lack of precision may mean that the solver cannot be
 sure which integer is intended, in which case the solver starts
 behaving more like an interval solver than a traditional finite
 domain solver. Note however that this precision limit is way beyond
 what is normally supported by finite domain solvers (typically
 substantially less than 2<SUP>32</SUP>). Note also that deliberately
 working with integer variables in this kind of range is not
 particularly recommended; the main intention is for the computation
 to be &#8220;safe&#8221; if it strays up into this region by ensuring no
 overflow problems.<BR>
<BR>
<LI CLASS="li-itemize">IC usually requires that expressions constructed at runtime be
 wrapped in <B>eval/1</B> when they appear in constraints; otherwise
 the variable representing the express may be assumed to be an IC
 variable, resulting in a type error. See section&nbsp;<A HREF="#sec:eval">3.1.7</A> for
 more details. We hope to remove this limitation in a future release.<BR>
<BR>
<LI CLASS="li-itemize">IC does not support the <A HREF="../bips/lib/fd/HLE-2.html"><B>#&lt;=/2</B></A><A NAME="@default7"></A>
 syntax for less-than-or-equal constraints. Use
 <A HREF="../bips/lib/ic/HEL-2.html"><B>#=&lt;/2</B></A><A NAME="@default8"></A> (the standard
	ECL<SUP><I>i</I></SUP>PS<SUP><I>e</I></SUP> operator for integer less-than-or-equal constraints)
	instead. Similarly, use
	<A HREF="../bips/lib/ic/HRE-2.html"><B>#\=/2</B></A>
 <A NAME="@default9"></A>
 instead of <A HREF="../bips/lib/fd/HH-2.html"><B>##/2</B></A><A NAME="@default10"></A>.<BR>
<BR>
<LI CLASS="li-itemize">The reified connectives provided by the two solvers are different:
 FD's
 <A HREF="../bips/lib/fd/HRP-1.html"><B>#\+/1</B></A>,
 <A NAME="@default11"></A>
 <A HREF="../bips/lib/fd/HFR-2.html"><B>#/\/2</B></A>,
 <A NAME="@default12"></A>
 <A HREF="../bips/lib/fd/HRF-2.html"><B>#\//2</B></A>,
 <A NAME="@default13"></A>
 <A HREF="../bips/lib/fd/HEG-2.html"><B>#=&gt;/2</B></A><A NAME="@default14"></A> and
 <A HREF="../bips/lib/fd/HLEG-2.html"><B>#&lt;=&gt;/2</B></A><A NAME="@default15"></A>
 (and their reified versions)
 correspond to IC's
 <A HREF="../bips/lib/ic/neg-1.html"><B>neg/1</B></A><A NAME="@default16"></A>,
 <A HREF="../bips/lib/ic/and-2.html"><B>and/2</B></A><A NAME="@default17"></A>,
 <A HREF="../bips/lib/ic/or-2.html"><B>or/2</B></A><A NAME="@default18"></A>,
 <A HREF="../bips/lib/ic/EG-2.html"><B>=&gt;/2</B></A><A NAME="@default19"></A> and
 <A HREF="../bips/lib/ic/HE-2.html"><B>#=/2</B></A><A NAME="@default20"></A>
 (and their reified versions).
 Note that IC has better reification support, in that any constraint
 may be embedded in any other constraint expression, evaluating to
 that constraint's reified value.<BR>
<BR>
<LI CLASS="li-itemize">The primitives for accessing and manipulating the domains of
 variables are different; see the section on variable query
	predicates (section&nbsp;<A HREF="libman018.html#domain-query">3.2.7</A>)
 for details of IC's support for this.</UL>
<A NAME="toc13"></A>
<H3 CLASS="subsection"><A NAME="htoc29">3.1.3</A>&nbsp;&nbsp;Differences between IC and RIA</H3>
The main difference between IC's interval solving and RIA's is that IC is
aware of and utilises the bounded real numeric type.
This means bounded reals may appear in IC constraints, and IC variables may
be unified with bounded reals (though direct unification is not recommended:
it is preferable to use an equality constraint to do the assignment).
In contrast, RIA will fail with a type error if bounded reals are used in
either of these cases.<BR>
<BR>
<A NAME="toc14"></A>
<H3 CLASS="subsection"><A NAME="htoc30">3.1.4</A>&nbsp;&nbsp;Notes about interval arithmetic</H3>
The main problem with using floating point arithmetic instead of real
arithmetic for doing any kind of numerical computation or constraint solving
is that it is only approximate. Finite precision means a floating point
value may only approximate the intended real; it also means there may be
rounding errors when doing any computation. Worse is that one does not know
from looking at an answer how much error has crept into the computation; it
may be that the result one obtains is very close to the true solution, or it
may be that the errors have accumulated to the point where they are
significant. This means it can be hard to know whether or not the answer
one obtains is actually a solution (it may have been unintentionally
included due to errors), or worse, whether or not answers have been missed
(unintentionally excluded due to errors).<BR>
<BR>
Interval arithmetic is one way to manage the error problem. Essentially
each real number is represented by a pair of floating point bounds. The
true value of the number may not be known, but it is definitely known to lie
between the two bounds. Any arithmetic operation to be performed is then
done using these bounds, with the resulting interval widened to take into
account any possible error in the operation, thus ensuring that the resulting
interval contains the true answer. This is the principle behind the bounded
real arithmetic type.<BR>
<BR>
Note that interval arithmetic does not guarantee small errors, it just
provides a way of knowing how large the error may have become.<BR>
<BR>
One drawback of the interval approach is that arithmetic comparisons can no
longer always be answered with a simple &#8220;yes&#8221; or &#8220;no&#8221;; sometimes the
only possible answer is &#8220;don't know&#8221;. This is reflected in the behaviour
of arithmetic comparators (=:=, &gt;=, etc.) when applied to bounded reals
which overlap each other. In such a case, one cannot know whether the true
value of one is greater than, less than, or equal to the other, and so a
delayed goal is left behind. This delayed goal indicates that the
computation succeeded, contingent on whether the condition in the delayed
goal is true. For example, if the delayed goal left behind was
<CODE>0.2__0.4 &gt;= 0.1__0.3</CODE>, this indicates that the computation should be
considered a success only if the true value represented by the bounded real
on the left is greater than or equal to that of the bounded real on the
right. If the width of the intervals in any such delayed goals is
non-trivial, then this indicates a problem with numerical accuracy. It is
up to the user to decide how large an error is tolerable for any given
application.<BR>
<BR>
<A NAME="toc15"></A>
<H3 CLASS="subsection"><A NAME="htoc31">3.1.5</A>&nbsp;&nbsp;Interval arithmetic and IC</H3>
In order to ensure the soundness of the results it produces, the IC
solver does almost all computation using interval arithmetic. As part
of this, the first thing done to a constraint when it is given to the
solver is to convert all non-integer numbers in it to bounded reals.
Note that for this conversion, floating point numbers are assumed to
refer to the closest representable float value, as per the type
conversion predicate
<A HREF="../bips/kernel/arithmetic/breal-2.html"><B>breal/2</B></A><A NAME="@default21"></A>.
This lack of widening when converting floating point numbers to
bounded reals is fine if the floating point number is exactly 
the intended real number, but if there is any uncertainty, that 
uncertainty should be encoded by using a bounded real in the 
constraint instead of a float.<BR>
<BR>
One of the drawbacks of this approach is that the user is not
protected from the fundamental inaccuracies that may occur when trying
to represent decimal numbers with floating point values in binary.
The user should be aware therefore that some numbers given explicitly
as part of their program may <EM>not</EM> be safely represented as a
bounded real that spans the exact decimal value. e.g.
<CODE>X $= 0.1</CODE> or equivalently <CODE>X is breal(0.1)</CODE>.<BR>
<BR>
This may lead to unexpected results such as
<PRE CLASS="verbatim">
[eclipse 2]: X $= 0.1, Y $= 0.09999999999999999, X $&gt; Y.

X = 0.1__0.1
Y = 0.099999999999999992__0.099999999999999992
Yes (0.00s cpu)

[eclipse 3]: X $= 0.1, Y $= 0.099999999999999999, X $&gt; Y.

No (0.00s cpu)
</PRE>
This potential source of confusion arises only with values which are
explicitly given within a program. By replacing the assignment to Y
with an expression which evaluates to the same real value we get
<PRE CLASS="verbatim">
[eclipse 4]: X $= 0.1, Y $= 0.1 - 0.000000000000000001, X $&gt; Y.

X = 0.1__0.1
Y = 0.099999999999999992__0.1


Delayed goals:
        ic : (0 &gt; -1.3877787807814457e-17__-0.0)
Yes (0.00s cpu)
</PRE>
Note the delayed goal indicating the conditions under which the original goal should be considered to have succeeded.<BR>
<BR>
<A NAME="toc16"></A>
<H3 CLASS="subsection"><A NAME="htoc32">3.1.6</A>&nbsp;&nbsp;Usage</H3>
To load the IC library into your program, simply add the following directive
at an appropriate point in your code.
<BLOCKQUOTE CLASS="quote">
<PRE CLASS="verbatim">
:- lib(ic).
</PRE></BLOCKQUOTE>
<A NAME="toc17"></A>
<H3 CLASS="subsection"><A NAME="htoc33">3.1.7</A>&nbsp;&nbsp;Arithmetic Expressions</H3>
The IC library solves constraint problems over the reals. It is not
limited to linear constraints, so it can be used to solve general problems
like:
<PRE CLASS="verbatim">
[eclipse 2]: ln(X) $&gt;= sin(X).

X = X{0.36787944117144228 .. 1.0Inf}


Delayed goals:
...
Yes (0.01s cpu)
</PRE>The IC library treats linear and non-linear constraints
differently. Linear constraints are handled by a single propagator,
whereas non-linear constraints are broken down into simpler
ternary/binary/unary propagators.<BR>
<BR>
Any relational constraint (<CODE>$=</CODE>, <CODE>$&gt;=</CODE>, <CODE>#=</CODE>, etc.)
can be reified simply by including it in an expression where it will 
evaluate to its reified truth value.<BR>
<BR>
User-defined constraints may also be included in constraint expressions
where they will be treated in a similar manner to user defined
functions found in expressions handled by <CODE>is/2</CODE>. That is to say
they will be called at run-time with an extra argument to collect the
result. Note, however, that user defined constraint/functions, when used
in IC, should be deterministic. User defined constraints/functions which
leave choice points may not behave as expected.<BR>
<BR>
Variables appearing in arithmetic IC constraints at compile-time are
assumed to be IC variables unless they are wrapped in an <B>eval/1</B>
term. See section&nbsp;<A HREF="#sec:eval">3.1.7</A> for an more detailed explanation of
usage.<BR>
<BR>
The following arithmetic expression can be used inside the constraints:
<DL CLASS="description" COMPACT=compact><DT CLASS="dt-description">
<B><TT>X</TT></B><DD CLASS="dd-description">
 <EM>Variables</EM>. If <CODE>X</CODE> is not yet a interval variable,
 it is turned into one by implicitly constraining it to be a real
 variable.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>123</TT></B><DD CLASS="dd-description">
 Integer constants. They are assumed to be exact and are used
 as is.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>0.1</TT></B><DD CLASS="dd-description">
 Floating point constants. These are assumed to be exact and
 are converted to a zero width bounded reals.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>pi, e</TT></B><DD CLASS="dd-description">
 Intervals enclosing the constants &pi; and <I>e</I> respectively.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>inf</TT></B><DD CLASS="dd-description">
 Floating point infinity.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>+Expr</TT></B><DD CLASS="dd-description">
 Identity.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>-Expr</TT></B><DD CLASS="dd-description">
 Sign change.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>+-Expr</TT></B><DD CLASS="dd-description">
 <CODE>Expr</CODE> or <CODE>-Expr</CODE>. The result is an interval
 enclosing both. If however, either bound is infeasible then
 the result is the bound that is feasible. If neither bound is
 feasible, the goal fails.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>abs(Expr)</TT></B><DD CLASS="dd-description">
 The absolute value of Expr.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>E1+E2</TT></B><DD CLASS="dd-description">
 Addition.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>E1-E2</TT></B><DD CLASS="dd-description">
 Subtraction.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>E1*E2</TT></B><DD CLASS="dd-description">
 Multiplication.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>E1/E2</TT></B><DD CLASS="dd-description">
 Division.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>E1</TT></B><B>^<TT>E2</TT></B><DD CLASS="dd-description">
 Exponentiation.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>min(E1,E2)</TT></B><DD CLASS="dd-description">
 Minimum.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>max(E1,E2)</TT></B><DD CLASS="dd-description">
 Maximum.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>sqr(Expr)</TT></B><DD CLASS="dd-description">
 Square. Logically equivalent to <CODE>Expr*Expr</CODE>, but with better 
 operational behaviour.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>sqrt(Expr)</TT></B><DD CLASS="dd-description">
 Square root (always positive).<BR>
<BR>
<DT CLASS="dt-description"><B><TT>exp(Expr)</TT></B><DD CLASS="dd-description">
 Same as <CODE>e^Expr</CODE>.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>ln(Expr)</TT></B><DD CLASS="dd-description">
 Natural logarithm, the reverse of the exp function.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>sin(Expr)</TT></B><DD CLASS="dd-description">
 Sine.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>cos(Expr)</TT></B><DD CLASS="dd-description">
 Cosine.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>atan(Expr)</TT></B><DD CLASS="dd-description">
 Arcus tangens. (Returns value between -pi/2 and pi/2.)<BR>
<BR>
<DT CLASS="dt-description"><B><TT>rsqr(Expr)</TT></B><DD CLASS="dd-description">
 Reverse of the sqr function. Equivalent to <CODE>+-sqrt(Expr)</CODE>.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>rpow(E1,E2)</TT></B><DD CLASS="dd-description">
 Reverse of exponentiation. i.e. finds <CODE>X</CODE> in <CODE>E1 = X^E2</CODE>.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>sub(Expr)</TT></B><DD CLASS="dd-description">
 A subinterval of Expr.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>sum(ExprList)</TT></B><DD CLASS="dd-description">
 Sum of a list of expressions.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>min(ExprList)</TT></B><DD CLASS="dd-description">
 Minimum of a list of expressions.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>max(ExprList)</TT></B><DD CLASS="dd-description">
 Maximum of a list of expressions.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>and</TT></B><DD CLASS="dd-description">
 Reified constraint conjunction. e.g. <CODE>B #= (X$&gt;3 and X$&lt;8)</CODE><BR>
<BR>
<DT CLASS="dt-description"><B><TT>or</TT></B><DD CLASS="dd-description">
 Reified constraint disjunction. e.g. <CODE>B #= (X$&gt;3 or X$&lt;8) </CODE><BR>
<BR>
<DT CLASS="dt-description"><B><TT>=&gt;</TT></B><DD CLASS="dd-description">
 Reified constraint implication. e.g. <CODE>B #= (X$&gt;3 =&gt; X$&lt;8) </CODE><BR>
<BR>
<DT CLASS="dt-description"><B><TT>neg</TT></B><DD CLASS="dd-description">
 Reified constraint negation. e.g. <CODE>B #= (neg X$&gt;3) </CODE><BR>
<BR>
<DT CLASS="dt-description"><B><TT>$&gt;</TT></B><B>, <TT>$&gt;=</TT></B><B>, <TT>$=</TT></B><B>, <TT>$=&lt;</TT></B><B>, <TT>$&lt;</TT></B><B>, <TT>$\=</TT></B><B>,
 <TT>#&gt;</TT></B><B>, <TT>#&gt;=</TT></B><B>, <TT>#=</TT></B><B>, <TT>#=&lt;</TT></B><B>, <TT>#&lt;</TT></B><B>,
 <TT>#\=</TT></B><B>,
 <TT>&gt;</TT></B><B>, <TT>&gt;=</TT></B><B>, <TT>=:=</TT></B><B>, <TT>=&lt;</TT></B><B>, <TT>&lt;</TT></B><B>, <TT>=\=</TT></B><B>,
 <TT>and</TT></B><B>, <TT>or</TT></B><B>, <TT>=&gt;</TT></B><B>, <TT>neg</TT></B><DD CLASS="dd-description">
 Any arithmetic or logical constraint that can be issued as a
 goal may also appear within an expression.<BR>
<BR>
Within the expression context, the constraint evaluates to its
 reified truth value. If the constraint is entailed by the
 state of the constraint store then the (sub-)expression
 evaluates to <CODE>1</CODE>. If it is dis-entailed by the state of
 the constraint store then it evaluates to <CODE>0</CODE>. If its
 reified status is unknown then it evaluates to an integral
 variable <CODE>0..1</CODE>.<BR>
<BR>
Note: The simple cases (e.g. <CODE>Bool #= (X #&gt; 5)</CODE>) are
 equivalent to directly calling the reified forms of the basic
 constraints (e.g. <CODE>#&gt;(X, 5, Bool)</CODE>).<BR>
<BR>
<DT CLASS="dt-description"><B><TT>foo(Arg1, Arg2 ... ArgN), module:foo(Arg1, Arg2 ... ArgN)</TT></B><DD CLASS="dd-description">
 Any terms found in the expression whose principle functor is
 not listed above will be replaced in the expression by a newly
 created auxiliary variable. This same variable will be
 appended to the term as an extra argument, and then the term
 will be called as <CODE>call(foo(Arg1, Arg2 ... ArgN, Aux))</CODE>.
 If no lookup module is specified, then the current
 module will be used.<BR>
<BR>
This behaviour mimics that of
 <A HREF="../bips/kernel/arithmetic/is-2.html"><B>is/2</B></A><A NAME="@default22"></A>.<BR>
<BR>
<DT CLASS="dt-description"><B><TT>eval(Expr)</TT></B><DD CLASS="dd-description">
 See section&nbsp;<A HREF="#sec:eval">3.1.7</A> for an explanation of <B>eval/1</B> usage.
</DL>

<H4 CLASS="subsubsection"><B>eval</B></H4>
<A NAME="sec:eval"></A>
The <B>eval/1</B> wrapper inside arithmetic constraints is used to
indicate that a variable will be bound to an expression at run-time.
This feature will only be used by programs which generate their
constraints dynamically at run-time, for example.
<PRE CLASS="verbatim">
broken_sum(Xs,Sum):-
    (
        foreach(X,Xs),
        fromto(Expr,S1,S2,0)
    do
        S1 = X + S2
    ),
    Sum $= Expr.
</PRE>The above implementation of a summation constraint will not work as
intended because the variable <TT>Expr</TT> will be treated like an IC
variable when it is in fact the term <TT>+(X1,+(X2,+(...)))</TT>
which is constructed in the for-loop.
In order to get the desired functionality, one must wrap the variable
<TT>Expr</TT> in an <B>eval/1</B>.
<PRE CLASS="verbatim">
working_sum(Xs,Sum):-
    (
        foreach(X,Xs),
        fromto(Expr,S1,S2,0)
    do
        S1 = X + S2
    ),
    Sum $= eval(Expr).
</PRE>
<HR>
<A HREF="libman016.html"><IMG SRC ="contents_motif.gif" ALT="Up"></A>
<A HREF="libman018.html"><IMG SRC ="next_motif.gif" ALT="Next"></A>
</BODY>
</HTML>
